package edu.uic.cs.cs582.process;

import java.util.Map;
import java.util.Set;

import org.sat4j.specs.TimeoutException;

import edu.uic.cs.cs582.data.SynsetSet;
import edu.uic.cs.cs582.data.Synset;
import edu.uic.cs.cs582.data.Word;
import edu.uic.cs.cs582.process.impl.SatIndexParser.Index;

/**
 * Process SAT
 * 
 * @author Hong Wang
 *
 */
public interface SatProcessor
{
	/**
	 * invoke sat solver to solve SAT problem
	 * 
	 * @param cnfArrays
	 * @return true, if there is no inconsistencies
	 * @throws TimeoutException
	 */
	//	boolean processSat(int[][] cnfClauses) throws TimeoutException;

	boolean processSat(Map<int[], Index> indicesByCnfClause)
			throws TimeoutException;

	/**
	 * Return the inconsistent words grouped by synset;
	 * 
	 * Notice: 
	 * Each word in which EACH majority-synset of the word contains 
	 * at least an inconsistent synset is inconsistent.
	 * 
	 * @return inconsistent words grouped by synset
	 */
	Map<Synset, Set<Word>> getConflictWordsBySynset();

	Map<SynsetSet, Set<Word>> getConflictWordsBySynsetsInMajority();

}
